a, b:. y:. GCD(a;b;y) 

latex

Definitions	AB, x:A. B(x), Dec(P), P  Q, t  T, , P  Q, P & Q, x. t(x), P  Q, P  Q, GCD(a;b;y), A, False
Lemmas	gcd p wf, gcd p neg arg 2, exists functionality wrt iff, le wf, gcd exists n, decidable le